$\forall$$T$:Type$_{\mbox{\scriptsize i}}$, $S$:(($\mathbb{N}\rightarrow$$T$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$). $T$ $\Rightarrow$ generic\{i:l\}($T$; $f$.$S$($f$)) $\Rightarrow$ ($\exists$$f$:($\mathbb{N}\rightarrow$$T$). $S$($f$))